Ein berühmtes Beispiel für ein formales System ist das MU Rätsel aus dem Buch Gödel, Escher, Bach, im die Beweisbarkeit eines formalen "Satzes" und der Bezug formaler Systeme zu den Axiomensystemen der Mathematik deutlich wird:

Douglas R. Hofstadter erfand dieses System, um die Anwendung von formalen Systemen in dem Bereich der Logik und Mathematik zu veranschaulichen. Es ist ein sehr einfaches System, das ca. drei Symbole und vier Regeln enthält. Schon die Grundrechenarten der Arithmetik, ebenfalls ein formales System, sind wesentlich komplexer. Da das System keine Entsprechungen für reale Dinge hat, in dem Gegensatz z.B. zu Zahlwörtern, wird der formale Charakter besonders deutlich. In dem formalen System spielt ja exakt die Bedeutung der Symbole keine Rolle mehr.

Das System besteht aus den drei Symbolen M, I und U. Symbolketten können durch die folgenden vier Regeln in andere Ketten verwandelt werden:

Regel1: Wenn das letzte Symbol I ist, kann U angefügt werden (aus MI wird MIU)

Regel2: Aus Mx kann Mxx erzeugt werden (aus MIU wird MIUIU)

Regel3: III kann durch U ersetzt werden (aus MUIIII wird MUIU)

Regel4: UU kann gestrichen werden (aus MUUUI wird MUI)

x in Regel2 steht für eine beliebige Symbolkette. xx bedeutet die Verdoppelung der Kette, diese wird also zweimal hinterander gesetzt.

Die Regeln dürfen in beliebiger Reihenfolge auf eine Symbolkette angewendet werden, auch mehrmals hintereinander.

1. MI
2. MII (Regel2)
3. MIIII (Regel2)
4. MUI (Regel3)
5. MUIU (Regel1)
6. MUIUUIU (Regel2)
7. MUIIU (Regel4)

1. Vorgegeben ist die Symbolkette MI
2. Gibt es eine Folge der Anwendung der Regeln, so dass die Symbolkette MU aus MI entsteht?

Die Aufgabe kann nicht durch einfaches Erzeugen aller möglichen Symbolketten (Brute Force-Suche) gelöst werden.

Die Lösung des Rätsels steht am Schluss des Artikels

Axiome sind Sätze, die von vornherein als wahr vorausgesetzt werden. In Axiomensystemen existieren meist ca. einige wenige Axiome. Die euklidische Geometrie hat z.B. ca. fünf Axiome.

Im formalen System lassen sich Axiome durch Symbolfolgen darstellen. In dem MU-Rätsel ist MI das einzige Axiom. Dieses ist also nach Definition wahr. Mit Hilfe der Umwandlungsregeln lassen sich aus den Axiomen andere Symbolfolgen erzeugen. Der Wahrheitswert ändert sich bei Anwendung dieser Regeln nicht, daher gelten die abgeleiteten Symbolketten ebenfalls als wahr.

Eine Symbolkette wird als mathematischer oder logischer Satz genannt. Die Axiom-Symbolketten sind daher in jedem Fall auch Sätze. Auch die durch Umwandlung erzeugten Symbolketten sind Sätze, genauso wie jede beliebige Symbolfolge.

Kennt man eine Folge der Anwendung der Regeln, die einen Satz aus den Axiom-Symbolketten erzeugt, so ist der Satz wahr. Die Folge ist der Beweis dieses Satzes. Sätze, für die grundsätzlich ein Beweis exisitiert, bezeichnet man beweisbar. Da sich normalerweise nicht jede Symbolkette erzeugen läßt, gibt es beweisbare und nicht beweisbare Sätze.

Im formalen System ist ein Satz beweisbar, wenn es grundsätzlich möglich ist, ihn durch Umwandlung aus den Axiomen zu erzeugen. Das MU-Rätsel fragt nach der Beweisbarkeit des "Satzes" MU. Hier darf man nicht Beweis und Beweisbarkeit verwechseln. Kennt man einen Beweis, so ist damit die Beweisbarkeit nachgewiesen. Es ist jedoch nicht stets nötig oder möglich, einen Beweis zu finden. Trotzdem können unter Umständen Aussagen zur Beweisbarkeit oder Nichtbeweisbarkeit gemacht werden, obwohl man den Beweis selbst nicht kennt.

Benutzt man ein Symbol zu dem Ausdrücken der Verneinung (z. B. ) und definiert, dass nicht wahr gleich falsch ist, so ist ein System widerspruchsfrei, wenn nicht gleichzeitig ein Satz und seine Verneinung bewiesen werden kann.

Beweisbare Sätze sind nach Definition immer wahr. In den meisten formalen Systemen können Sätze formuliert werden, die weder beweis- noch widerlegbar sind. Widerlegung ist dabei der Beweis der Verneinung. Man kann ein formales System dann erweiteren, indem man für einen solchen Satz einfach definiert, ob er wahr oder falsch ist. In dem erweiterten System existiert dann ein Beweis oder eine Widerlegung, nämlich einfach die hinzugefügte Definition.

Erstaunlicherweise kann man jedoch nicht jedes System so erweitern, dass alle Sätze auch beweis- oder widerlegbar sind. In manchen Systemen bleiben immer unentscheidbare Sätze übrig. Dies hat Kurt Gödel 1930 mit seinem Unvollständigkeitssatz zweifelsfrei nachgewiesen.

Logiksysteme wie die Aussagenlogik können durch ein formales System definiert werden. Dazu könnte man normale Wörter wie und, oder, nicht benutzen, was die Verständlichkeit erhöhen würde. Allerdings haben solche Wörter immer Nebenbedeutungen, die den exakten Charakter der Aussagen nicht widerspiegeln. Daher werden neue Symbole eingeführt, deren Interpretation keinen Freiraum mehr bietet:

Die folgende Tabelle gibt Symbole wieder, die zu einer Definition der Aussagenlogik dienen können:

Symbol	Beschreibung
A B C ...	Aussage. Eine Aussage wird durch einen Grossbuchstaben repräsentiert.
	nicht. Verneinung einer Aussage ist exakt dann wahr, wenn A falsch ist, und umgekehrt.
	und. Die Gesamtaussage ist exakt dann wahr, wenn sowohl A als auch B wahr sind.
	oder. Die Gesamtaussage ist exakt dann wahr, wenn entweder A oder B oder beide wahr sind.
	ist gleichwertig zu. Die Gesamtaussage ist wahr, wenn A und B beide wahr oder beide falsch sind.
	aus folgt. Die Folgerung ist falsch, wenn A wahr, aber B dennoch falsch ist. In allen anderen Fällen ist wahr.
( )	Klammern. Klammern dienen dazu, die Ausführung einer Operation vor einer anderen zu erzwingen, wenn Unklarheiten bestehen.

In formalen Systemen entspricht ein Satz exakt einer Folge von Symbolen, also einer Symbolkette, etwa

Satz:

Übersetzt heißt dies: Die Aussage "A und B" hat denselben Wahrheitswert wie die Verneinung der Aussage "nicht A oder nicht B".

Ein Satz kann wahr oder falsch sein.

Symbolfolgen kann man in formalen Systemen über Regeln in andere Symbolfolgen umformen. Zur Definition der zugelassenen Regeln kann man auch ein (einfacheres) formales System benutzen:

Symbol	Beschreibung
a b c ...	Symbolfolge. Ein Kleinbuchstabe kann durch eine Symbolfolge ersetzt werden. Gleiche Kleinbuchstaben in einer Folge müssen durch gleiche Symbolfolgen ersetzt werden.
	kann ersetzt werden durch. Die Symbolfolge auf der linken Seite kann durch die Folge auf der rechten Seite ersetzt werden, ohne den Wahrheitsgehalt zu ändern. Ebenso kann die rechte Folge durch die linke ersetzt werden.
wahr falsch	Symbole für eindeutig wahre und falsche Aussagen

Symbole für Umwandlungsregeln (Beispiel)

Eine Umwandlungsregel könnte dann so aussehen:

Schlussregel1:

.

Dies bedeutet, dass man auf der linken Seite jedes Satzes entfernen oder hinzufügen darf. Umgangssprachlich entspricht dies der doppelten Verneinung:

Schlussregel1: Die Verneinung der Verneinung einer Aussage ist die Aussage selbst

Weitere Umwandlungsregeln sind z.B.

Schlussregel2:
Schlussregel3:
Schlussregel4:
Schlussregel5:
Schlussregel6:
Schlussregel7:

Die Punkte deuten an, dass noch viele weitere Umwandlungsregeln definiert werden können. Dies sind die Schlussfolgerungs-Regeln für die formale Logik. Sie können rein formal ohne Bezug zur Bedeutung der Symbole angewendet werden. Damit verhalten sich die Regeln wie Rechenregeln.

Trotzdem wurden die Regeln "sinnvoll" gewählt. Schlussregel3 bedeutet, dass eine wahre Aussage oder eine beliebige Aussage als Gesamtaussage stets wahr ist. Dagegen bedeutet die kompliziertere Schlussregel5 (Folgerung) übersetzt etwa:

Schlussregel5: aus a folgt b kann ersetzt werden durch die Aussage "Verneinung von Aussage a oder Aussage b".

Die Folgerung ist exakt dann falsch, wenn a wahr, aber b dennoch falsch ist. Umgekehrt ist sie also wahr, wenn a falsch oder wenn b wahr ist. Dies entspricht formal (lies: nicht a oder b).

Ein Beweis besteht aus einer Behauptung und einer Schlussfolgerung. In dem formalen System wird eine Behauptung b als Symbolfolge dargestellt, ebenso die Schlussfolgerung s. Der Beweis wird geführt, indem der Satz "aus der Behauptung folgt die Schlussfolgerung" in wahr umgewandelt wird:

Formaler Beweis:

(aus der Behauptung b folgt die Schlussfolgerung s) kann mit Hilfe der Umwandlungsregeln überführt werden in wahr.

Beweis des Satzes: Aus Falschem folgt Beliebiges

Der klassische Satz ex falsum quod libet (aus Falschem folgt Beliebiges) kann formal dargestellt und bewiesen werden. In unserem formalen System lautet er:

Die Folgerung aus einer falschen Aussage ist stets wahr

Beweis:

Zum Beweis wenden wir die Umformungsregel für die Folgerung an:

(Schlussregel5)

Nicht falsch ist aber wahr:

(Schlussregel2)

Schließlich ist eine wahre Aussage oder Beliebiges stets war.

wahr (Schlussregel3)

Der Satz ist damit formal bewiesen. Der Beweis könnte durch ein Computerprogramm erfolgen, das ca. die Symbole kennt und die Schlussregeln anwendet.